#include <stdint.h>

int main() {
    uint64_t value = 0x123456789ABCDEF0;

    uint64_t* ptr = &value;

    uint64_t loaded_value = *ptr;

    return (int)loaded_value;
}
